{-# LANGUAGE ExistentialQuantification, QuasiQuotes, TypeOperators,
  Rank2Types, GADTs, ScopedTypeVariables, TypeFamilies, FlexibleContexts,
  TemplateHaskell #-}

{- |

Module      :  Type.Yoko.Natural
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Natural transformations and pairs.

-}

module Type.Yoko.Natural where

import Type.Yoko.Type
import Type.Yoko.SetModel



type SynNT u f = forall t. u t -> f t

-- | Natural transformations. We use 'Unwrap' to lighten the user interface at
-- the value level, though it clutters the types a little.
newtype NT u f = NT (forall t. u t -> Unwrap f t)

nt :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f
nt p f = NT f


appNT :: NT u f -> u t -> Unwrap f t
appNT (NT f) x = f x

appNTF :: Wrapper f => NT u f -> SynNT u f
appNTF (NT f) x = wrap (f x)


-- | Defining an @NT@ via type-level backtracking; ':||' uses 'Pred' to
-- short-circuit, preferring inhabitation of @u@ over @v@.
orNT :: NT u f -> NT v f -> NT (u :|| v) f
orNT (NT f) (NT g) = NT $ \uv -> case uv of
  LeftU  u -> f u
  RightU v -> g v

-- | @weakenOrNT fs gs@ builds an 'NT' that uses @fs@ for as many types in the
-- type set @v@ as possible, and uses @gs@ for the rest.
--
--   @eachOrNT fs dflt = firstNT weaken $ orNT fs dflt@
weakenOrNT :: (v :=> (u :|| w)) => NT u f -> NT w f -> NT v f
weakenOrNT fs dflt = firstNT weaken $ orNT fs dflt

constNT :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f
constNT p x = nt p $ \Refl -> x

constNTF :: Wrapper f => f t -> NT ((:=:) t) f
constNTF x = NT $ \Refl -> unwrap x


firstNT :: SynNT u v -> NT v f -> NT u f
firstNT embed (NT f) = NT $ f . embed





-- | Natural pairs.
data NP u f = forall t. NP (u t) (Unwrap f t)

-- | Analog to "Control.Arrow"@.first@.
firstNP :: SynNT u v -> NP u f -> NP v f
firstNP embed (NP u x) = NP (embed u) x


-- | @ArrowTSS@ can be partially applied, and hence occur as the second
-- argument of @NT@, where as @f _ -> g _@ cannot.
newtype ArrowTSS f g a = ArrowTSS (f a -> g a); wraps_thinly ''ArrowTSS

appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g
appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x
